T:Type, x:T, L:(T List). (x  L)  sublist(T; cons(x; []); L) 

latex

Definitions	suptype(S; T), subtype(S; T), False, A, t  ...$L, ge(i; j), A  B, prop{i:l}, t  T, Y, P  Q, P  Q, P  Q, ||as||, A c B, x:A. B(x), sublist(T; L1; L2), (x  l), P  Q, x:A. B(x), lelt(i; j; k), int_seg(i; j), increasing(f; k), ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), True, T, guard(T), sq_type(T), l[i],
Lemmas	non neg length, length cons, length nil, increasing wf, int seg wf, select wf, length wf1, nat wf, le wf